What is a proof assistant?

Meet Lean

A programming language where the statements are theorems and the programs are proofs — checked by an infinitely patient, extremely picky referee.

• Created in 2013 by Leonardo de Moura (then Microsoft Research, now AWS).
• Current version: Lean 4 — a real, fast programming language.
• Since 2023: backed by its own dedicated nonprofit, whose full-time job is usability, documentation, and proof automation.

Your first theorem

Taste of Lean

theorem two_plus_two : 2 + 2 = 4 := rfl

• two_plus_two — the name.
• 2 + 2 = 4 — the statement.
• rfl — the proof: “true by computation.”
• That’s the entire file. No imports. It compiles. It’s a theorem.

What happens when you lie

Taste of Lean

• Lean is not a search engine. Not a chatbot. Not “pretty confident.”
• It is incapable of accepting a false step.
• No “clearly.” No “trivially.” No hand-waving. Ever.

A proof with actual content

Taste of Lean

example (a b : Nat) :
    a + b = b + a := by
  induction b with
  | zero => simp
  | succ n ih =>
      rw [Nat.add_succ, ih,
          Nat.succ_add]

-- the goal window (sketch) --
case zero
⊢ a + 0 = 0 + a        ✓ simp

case succ
ih : a + n = n + a
⊢ a + (n+1) = (n+1) + a
  rw [Nat.add_succ] ↦
⊢ (a + n) + 1 = (n+1) + a
  rw [ih] ↦
⊢ (n + a) + 1 = (n+1) + a
  rw [Nat.succ_add] ↦  ✓

• induction, simp, rw are tactics: proof moves. The goal window is a blackboard that updates itself.

The most honest word in mathematics

Taste of Lean

theorem my_big_lemma : ∀ n : Nat, n + 0 = n := by
  sorry

• sorry = “I’ll prove this later.” Lean accepts it — with a loud warning.
• It’s how you sketch a big proof: state everything, sorry the gaps, fill them one by one.
• The gold standard of done: sorry-free.
• Remember Astra’s certificates? Sorry-free Lean proofs. Now you know what that means.
• Zero sorries. Nothing owed. Nowhere left for that 2am-fear to live.

How the checking actually works

Under the hood

• You write tactics; Lean’s elaborator turns your moves into a proof term — an actual, fully written-out program.
• The statement is a type; the proof term is a program of that type. That’s “proof = program,” made literal.
• A small, deliberately isolated kernel — a tiny fraction of the system — re-checks every proof term from scratch, against the rules of dependent type theory.
• You never trust the 2M-line library, the tactics, or the AI that drafted the proof. You trust the tiny kernel. Independent checkers can re-verify its verdicts.

Caveats — what “verified” doesn’t mean

Under the hood

• Lean certifies the proof of the statement you wrote. Mis-state the theorem → a flawless proof of the wrong thing.
• Definitions must match intent. Is your formal “atomic monoid” the atomic monoid? A human still reads the definitions.
• You still trust something: the kernel — and the axioms you opt into (e.g. classical logic). Lean will list them for any theorem.
• Verified ≠ illuminating. A compiled proof can still be unreadable. Insight stays our job.

Limitations — what it still costs

Under the hood

• Formalizing is slow. A page of paper math is usually many pages of Lean — and “obvious” steps are often the most expensive.
• The library is uneven. Astonishingly deep in places; blank in whole research areas.
• The learning curve is real. Comfort takes weeks of play, not one evening — that’s why this talk ends with an on-ramp.
• AI has entered research mathematics. Humans still frame problems, audit definitions, and validate novelty and significance.

Let’s prove one, live

No slides for two minutes — real Lean

Compute · automate · use the library — backup script in the appendix.

You don’t start from axioms alone

mathlib

mathlib — the community’s single, unified library of formalized mathematics.

Theorems you already know, on demand

mathlib

import Mathlib

#check Nat.exists_infinite_primes   -- ∀ n : ℕ, ∃ p, n ≤ p ∧ p.Prime
#check irrational_sqrt_two          -- Irrational √2

mathlib speaks this group’s language

Your objects, formally

-- faithful to mathlib4
structure Irreducible [Monoid M] (p : M) : Prop where
  not_isUnit : ¬IsUnit p
  isUnit_or_isUnit : ∀ a b, p = a * b → IsUnit a ∨ IsUnit b

[Monoid M] simply reads: “assuming M is a monoid.”

• Not a unit; any factorization p = a * b forces a unit. That is the definition of an atom from your factorization-theory papers.
• There’s AddIrreducible too — for additively written monoids. Hello, semidomains.
• Prime, Associated, Associates — the prime-vs-irreducible distinction this audience lives on is baked into the library’s bones.

The punchline definition

Your objects, formally

UFM = cancellative + ACCP + (irreducible ↔︎ prime).

class UniqueFactorizationMonoid (α : Type*) [CommMonoidWithZero α] : Prop
    extends IsCancelMulZero α, IsWellFounded α DvdNotUnit where
  irreducible_iff_prime {a : α} : Irreducible a ↔ Prime a

• IsCancelMulZero → cancellative · IsWellFounded α DvdNotUnit → ACCP · the field → atoms are prime
• mathlib refactored unique factorization into exactly the factorization-theorist’s viewpoint. Your field’s lens won.

Formalization at research speed

Landmark: PFR

Marton’s conjecture (Polynomial Freiman–Ruzsa):

• Nov 9, 2023 — Gowers, Green, Manners, Tao post the proof.
• Tao launches a crowdsourced Lean formalization, with Yael Dillies and Bhavik Mehta.
• Dec 5, 2023 — “no sorrys.” About three weeks, paper to machine-checked.

Sometimes the crowd is the theorem

Landmark: Equational Theories

Tao’s Equational Theories Project: for magmas — one set, one binary operation, this crowd’s home turf —

• 4,694 equational laws. 22,028,942 implications between them.
• Every single one settled — humans + automation; primary goal completed Apr 14, 2025, final report on arXiv Dec 2025.
• 50+ contributors, with genuine room for beginners.

And the long game

Landmark: FLT

Kevin Buzzard’s Fermat’s Last Theorem project (Imperial College London):

• Formalizing a 21st-century proof — not Wiles’s original.
• Funded by a UK national research grant through September 2029. Contributor workshop in London last month.
• A proof so big no single person will ever check it by hand — exactly why we’re building the machine that can.

AI’s problem, Lean’s superpower

LLMs draft, Lean checks

Language models are fluent, confident — and sometimes wrong.

• Oct 2025: OpenAI’s Kevin Weil announces GPT-5 “solved” 10 open Erdős problems…
• …but existing papers already contained the mathematics.
• Demis Hassabis: “embarrassing.”
• The mathematics was sound; the novelty claim was not.
• Lean checks a formal argument. It does not certify novelty or search the literature.

2024: the machine enters the IMO

LLMs draft, Lean checks

DeepMind’s AlphaProof + AlphaGeometry 2 system at IMO 2024 — the first AI system to reach medal level:

• Combined result: 4/6 problems, 28/42 points — one point below the gold cutoff.
• AlphaProof solved P1, P2, and P6, the hardest; AlphaGeometry 2 solved P4.
• AlphaProof trained AlphaZero-style, with Lean as the referee: only kernel-checked proofs count.
• Important caveats: humans translated the problems into Lean; some solutions took ~3 days of compute.

One year later

LLMs draft, Lean checks

IMO 2025:

• Gemini Deep Think: official gold, 35/42, in natural language, within the time limit.
• Harmonic’s Aristotle: 5/6 with Lean-verified proofs — no human grading needed.
• And the slope: undergrad competition problems (the Putnam) went from nearly untouched (2024) to ~88% solved (late 2025).

Correctness is not novelty

Lean checks proofs · people check context

• Lean verifies the formal argument — not novelty or literature precedence.
• Trustworthy AI mathematics needs both: machine-checked correctness and expert statement and literature review.

This story is already inside SWIM

Aug 11 · mark your calendar

Next week, in this same Zoom room:

“Finitely Generated Semidomains: Formalization and a Conjecture” — Jonathan Liu, Jason Yang, Alan Yao (MIT CMI students), Tuesday Aug 11.

• Fun fact: “semidomain” doesn’t exist in mathlib… yet.
• The people building it are in this workshop — fresh off the bi-UFS positive semidomains paper (arXiv:2607.22941).
• Come to that talk with tonight’s eyes.

Your objects, at the frontier

Closest to home

February 2026: Fel’s conjecture on syzygies of numerical semigroups (Chen, Lau, Ono, Zhang, et al.)

• A conjecture about numerical semigroups — this community’s bread and butter.
• The proof was fully formalized in Lean …
• … and the formalization was generated automatically by AxiomProver from the English statement of the theorem.

“Syzygies” is a technical invariant — the word doesn’t matter tonight. The objects — numerical semigroups — are yours.

Who’s going to change that?

Your math, in motion

• The formalization of this territory is being carried out by CMI students.
• The bulk of the work happens next CMI semester — your field will appear in mathlib, definition by definition, theorem by theorem.
• Aug 11 is the first installment: finitely generated semidomains, in this Zoom room.

Your on-ramp, in order

Start tonight

1. Tonight — the Natural Number Game: adam.math.hhu.de · 79 levels, in your browser, zero install. You’ll re-prove a + b = b + a yourself before bed.
2. This week — Glimpse of Lean (Patrick Massot): a 2–3 hour guided tour.
3. This month — Mathematics in Lean, the standard textbook. Experiment freely at live.lean-lang.org.
4. Always — the Lean Zulip chat: famously kind to newcomers. Ask anything.
5. Aug 11 — show up to the semidomains talk with new eyes.

Appendix: the live-demo script

Backup — only if the embedded editor won’t load

import Mathlib

#eval 2 + 2                         -- Lean computes: 4

example (a b : Nat) : a + b + 0 = b + a := by
  omega                             -- automation closes it

#check irrational_sqrt_two          -- Irrational √2
example : Irrational (Real.sqrt 2) := irrational_sqrt_two